Философская энциклопедия - исчисление логическое

Аксиомы представляют собой фиксируемый в языке исчисления набор исходных выражений, принимаемых непосредственно (как постулаты). Правила вывода это правила вида "из формул F1, ..., Fm выводима формула G", символическая запись: (F1, ..., Fm) G. Формулы F1, ..., Fm называются посылками вывода, a G заключением вывода. В каждом конкретном правиле формулы F1, ..., Fm, G имеют конкретный вид, число посылок (m) также принимает конкретное значение.

Приписывание символам исчисления значений, т. е. интерпретация, превращает исчисление в семантическую систему (формализованный язык) . И. л. представляет собой логически интерпретированное исчисление, изучение которого предполагает тщательное построение и анализ трех металогических уровней языка: синтаксического, семантического и прагматического. Доказательством формулы F в И. л. называется последовательность формул HI, ..., Hm, F, в которой каждая формула либо аксиома исчисления, либо выводима из некоторых предыдущих (т. е. уже доказанных) формул с помощью одного из правил вывода. Для каждого И. л. важное значение имеют вопросы о его непротиворечивости (в непротиворечивом исчислении не выводимы одновременно какое-либо выражение и его отрицание), полноте (исчисление является полным, если множество его истинных утверждений совпадает с множеством утверждений, доказуемых в нем), решении проблемы разрешимости (исчисление является разрешимым, если существует алгоритм, позволяющий для любого утверждения определять, выводимо оно в нем или нет) и др. Решение данных вопросов определяет логическую возможность интерпретации исчисления и является необходимым условием его практической реализуемости, Различные теории вывода представляют И. л., отличающиеся своими свойствами.

А. Г. Кислое